(declare-fun s0 () (_ FloatingPoint 4 5))
(declare-fun s1 () (_ FloatingPoint 4 5))
(declare-fun s17 () (_ BitVec 9))
(declare-fun s83 () (_ BitVec 9))
(assert s5)
(assert s6)
(assert s11)
(assert s12)
(assert s19)
(assert (= s82 s83))
(check-sat)
